(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (> (div b (- a)) 1))
(assert (> (* c (- (* a b) 2)) a))
(assert (> c 0))
(assert (not (<= a (- 1) 1 b)))
(assert (>= b a))
(check-sat)
